Nuprl Lemma : sqequal_1 |
13,42 |
|
COM: sqequal_1_begin
COM: sqequal_com
COM: sq_type_com
ABS: SQType(T)
STM: int sq
STM: nat sq
STM: bool sq
STM: atom sq
COM: case_ite_com
STM: bool sim true
STM: bool sim false
STM: eq int eq true intro
STM: eq int eq false intro
STM: lt int eq true elim
STM: lt int eq false elim
STM: eq atom eq true elim
STM: eq atom eq false elim
STM: eq int eq true elim sqequal
STM: eq int eq false elim sqequal
STM: lt int eq true elim sqequal
STM: lt int eq false elim sqequal
STM: eq atom eq true elim sqequal
STM: eq atom eq false elim sqequal
STM: bool cases sqequal
COM: sqequal_1_end